2.7.55 Rewrites Tutorial Exercise 4

Here is a suitable set of rules to solve the first part of the problem:

[ seq(n, c) := seq(n/2,  c+1) :: n%2 = 0,
  seq(n, c) := seq(3n+1, c+1) :: n%2 = 1 :: n > 1 ]

Given the initial formula ‘seq(6, 0)’, application of these rules produces the following sequence of formulas:

seq( 3, 1)
seq(10, 2)
seq( 5, 3)
seq(16, 4)
seq( 8, 5)
seq( 4, 6)
seq( 2, 7)
seq( 1, 8)

whereupon neither of the rules match, and rewriting stops.

We can pretty this up a bit with a couple more rules:

[ seq(n) := seq(n, 0),
  seq(1, c) := c,
  ... ]

Now, given ‘seq(6)’ as the starting configuration, we get 8 as the result.

The change to return a vector is quite simple:

[ seq(n) := seq(n, []) :: integer(n) :: n > 0,
  seq(1, v) := v | 1,
  seq(n, v) := seq(n/2,  v | n) :: n%2 = 0,
  seq(n, v) := seq(3n+1, v | n) :: n%2 = 1 ]

Given ‘seq(6)’, the result is ‘[6, 3, 10, 5, 16, 8, 4, 2, 1]’.

Notice that the ‘n > 1’ guard is no longer necessary on the last rule since the ‘n = 1’ case is now detected by another rule. But a guard has been added to the initial rule to make sure the initial value is suitable before the computation begins.

While still a good idea, this guard is not as vitally important as it was for the fib function, since calling, say, ‘seq(x, [])’ will not get into an infinite loop. Calc will not be able to prove the symbol ‘x’ is either even or odd, so none of the rules will apply and the rewrites will stop right away.